T:Type, eq:EqDecider(T), es:ES, x:Id, e, e':E.
@loc(e')(x:T)
 (e <loc e')
 ((x after lastchange(x;e')) = (x when lastchange(x;e'))  T)
 ((x after e) = (x when e')  T) 

latex

Definitions	True, T, {T}, SQType(T), P  Q, P  Q, P & Q, , t  T, P  Q, EqDecider(T), x:A. B(x), (e <loc e'), x:A. B(x), ee'.P(e), False, A, @e(xv), A c B, ff, tt, P  Q, if b then t else f fi , lastchange(x;e), @i(x:T)
Lemmas	es-locl-iff, es-loc-pred, true wf, squash wf, es-le-loc, es-after-pred2, es-next, not-changed, last-change-property, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bool sq, bool cases, not wf, bnot wf, changed wf, assert wf, iff wf, bool wf, event system wf, Id wf, es-E wf, es-locl wf, es-when wf, es-vartype wf, es-loc-lc, es-loc wf, es-dtype wf, es-lc wf, es-after wf